Section: New Results

Formal study of a cell-decomposition algorithm

Participants : Julien Lamiroy, Yves Bertot.

To solve robot motion planning problems, a simple approach is to decompose the available space into obstacle-free cells and to more from one cell to another only by boundaries that are also obstacle free. We developed a formal description of an algorithm producing this kind of decomposition, with the aim of providing formal proofs of correctness in the long run.